/*
 * Param.java
 * 
 * Copyright 2004 Christoph Csallner and Yannis Smaragdakis.
 */
package edu.gatech.cc.cnc.params;

import static edu.gatech.cc.jcrasher.Assertions.notNull;
import static edu.gatech.cc.jcrasher.Constants.TAB;

import java.lang.reflect.Member;

import edu.gatech.cc.jcrasher.plans.expr.Variable;
import edu.gatech.cc.jcrasher.plans.stmt.Block;
import edu.gatech.cc.jcrasher.plans.stmt.BlockImpl;
import edu.gatech.cc.jcrasher.plans.stmt.BlockStatement;

/**
 * Represents a method parameter or some other variable.
 * <ul>
 * <li>
 * Initially, these are all values allowed by the Java semantics.
 * E.g., for int this ranges from Integer.MIN_VALUE to Integer.MAX_VALUE.
 * <li>
 * ESC/Java might give us some constraints on these parameters
 * (or variables). We reflect these constraints with the constrain
 * methods.
 * <li>
 * After applying (solving) the constraints we can retrieve
 * individual values from Param.
 * <li>
 * Note that ESC/Java may give us constraints that are
 * inconsistent with Java execution semantics or even
 * with themselves.
 * We do very little consistency checking in our constraint
 * solvers. We are lazy and just apply constraints as we parse them
 * and ignore some of them as we see fit.
 * Inconsistencies are definitely uncovered at test-runtime,
 * when our test cases do not reveal the bug ESC was warning of.
 * 
 * TODO: We could do more consistency checking in our constraint
 * solvers. Even better would be to fix ESC/Java so that
 * the constraints it emits are at least consistent among themselves.
 * 
 * @param <T> Type of method parameter/variable this represents.
 * 
 * @author csallner@gatech.edu(Christoph Csallner)
 */
public abstract class Param<T> {
	  
  protected static Block<?> block; //to create names for aliasing.
  protected static Class<?> testeeType;
  
  public static Block<?> getBlock() {
    return block;
  }  
  
  /**
   * To be called for each constraint system,
   * before any constraints are processed.
   * 
   * @param member method or constructor for which we will plan in fresh name context.
   * @param newTesteeType class of testee.
   */
  public static <U> void resetNames(Member member, Class<U> newTesteeType) {
    notNull(member);
    notNull(newTesteeType);
    
    block = new BlockImpl<U>(newTesteeType, member, TAB+TAB);
    testeeType = newTesteeType;
  }
  
  
  /**
   * @return unique identifier
   */
  public static <T> Variable<T> nextID(Class<T> type) { //TODO: Is static right here?
    return block.getNextID(type);
  }
  
  
	/**
	 * @return type name.
	 */
	public abstract String getTypeName();
	
	/**
	 * @return the type of the wrapped parameter.
	 * This might be a subtype if we applied a subtype
	 * constraint.
	 */
	public abstract Class<? extends T> getType();

	/**
	 * @return statement that declares a new variable
   * and assigns it the result of our constraint solving.
   * This might also be a statement sequence.
	 */
	public abstract BlockStatement<? extends T> getPlan();
	
	/**
	 * <code>constraint ::= constLHS relation2 this.</code>
	 * <p>
	 * relation2 refers to integer constants of sym.
	 */
	public abstract void constrain(String constLHS, int relation2);
	
	/**
	 * <code>constraint ::= this relation2 constRHS.</code>
	 */
	public abstract void constrain(int relation2, String constRHS);
		
	/**
	 * <code>constraint ::= this relation2 rhs.</code>
	 * <p>
	 * It would be nice if we would only have constraints between
	 * variables of the same type. Then rhs could be a Param<T>.
	 * But ESC/Java may generate constraints that involve variables of
	 * different types like (NEQ (typeof this) T_boolean).
	 */
	public abstract void constrain(int relation2, Param<?> rhs);

	
	
	/**
	 * Redundantly encode name of param to ease debugging.
	 */
	protected String name; 
  
	
	/**
	 * Constructor
	 */
	protected Param(String name) {
		
		this.name = notNull(name);
	}	
  
	@Override
	public String toString() {
		return name;
	}	
}
